Step of Proof: inv_image_ind_tp 9,38
Inference at * 1 
Iof proof for Lemma inv image ind tp:



1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
  WellFnd{i}(S;x,y.r(f(x),f(y))) 
latex
 by UnfoldTopAb 0 
latex

 1: 

 1:   P:(S). (j:S. (k:S. r(f(k),f(j))  P(k))  P(j))  {n:S. P(n)}
 .

DefinitionsWellFnd{i}(A;x,y.R(x;y))

origin